0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 89 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 72 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 5 ms)
↳16 QDP
↳17 QDPOrderProof (⇔, 35 ms)
↳18 QDP
↳19 DependencyGraphProof (⇔, 0 ms)
↳20 TRUE
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → U5_GG(X1, X2, X3, pB_in_ggag(X2, X3, X4, X1))
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → PB_IN_GGAG(X2, X3, X4, X1)
PB_IN_GGAG(X1, X2, X3, X4) → U2_GGAG(X1, X2, X3, X4, appendC_in_gga(X1, X2, X3))
PB_IN_GGAG(X1, X2, X3, X4) → APPENDC_IN_GGA(X1, X2, X3)
APPENDC_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U1_GGA(X1, X2, X3, X4, appendC_in_gga(X2, X3, X4))
APPENDC_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)
PB_IN_GGAG(X1, X2, X3, X4) → U3_GGAG(X1, X2, X3, X4, appendcC_in_gga(X1, X2, X3))
U3_GGAG(X1, X2, X3, X4, appendcC_out_gga(X1, X2, X3)) → U4_GGAG(X1, X2, X3, X4, lessleavesA_in_gg(X4, X3))
U3_GGAG(X1, X2, X3, X4, appendcC_out_gga(X1, X2, X3)) → LESSLEAVESA_IN_GG(X4, X3)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U6_GG(X1, X2, X3, X4, X5, appendC_in_gga(X2, X3, X6))
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → APPENDC_IN_GGA(X2, X3, X6)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U7_GG(X1, X2, X3, X4, X5, appendcC_in_gga(X2, X3, X6))
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → U8_GG(X1, X2, X3, X4, X5, pB_in_ggag(X4, X5, X7, cons(X1, X6)))
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → PB_IN_GGAG(X4, X5, X7, cons(X1, X6))
appendcC_in_gga(nil, X1, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U13_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U13_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → U5_GG(X1, X2, X3, pB_in_ggag(X2, X3, X4, X1))
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → PB_IN_GGAG(X2, X3, X4, X1)
PB_IN_GGAG(X1, X2, X3, X4) → U2_GGAG(X1, X2, X3, X4, appendC_in_gga(X1, X2, X3))
PB_IN_GGAG(X1, X2, X3, X4) → APPENDC_IN_GGA(X1, X2, X3)
APPENDC_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → U1_GGA(X1, X2, X3, X4, appendC_in_gga(X2, X3, X4))
APPENDC_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)
PB_IN_GGAG(X1, X2, X3, X4) → U3_GGAG(X1, X2, X3, X4, appendcC_in_gga(X1, X2, X3))
U3_GGAG(X1, X2, X3, X4, appendcC_out_gga(X1, X2, X3)) → U4_GGAG(X1, X2, X3, X4, lessleavesA_in_gg(X4, X3))
U3_GGAG(X1, X2, X3, X4, appendcC_out_gga(X1, X2, X3)) → LESSLEAVESA_IN_GG(X4, X3)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U6_GG(X1, X2, X3, X4, X5, appendC_in_gga(X2, X3, X6))
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → APPENDC_IN_GGA(X2, X3, X6)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U7_GG(X1, X2, X3, X4, X5, appendcC_in_gga(X2, X3, X6))
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → U8_GG(X1, X2, X3, X4, X5, pB_in_ggag(X4, X5, X7, cons(X1, X6)))
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → PB_IN_GGAG(X4, X5, X7, cons(X1, X6))
appendcC_in_gga(nil, X1, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U13_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U13_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
APPENDC_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)
appendcC_in_gga(nil, X1, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U13_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U13_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
APPENDC_IN_GGA(cons(X1, X2), X3, cons(X1, X4)) → APPENDC_IN_GGA(X2, X3, X4)
APPENDC_IN_GGA(cons(X1, X2), X3) → APPENDC_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → PB_IN_GGAG(X2, X3, X4, X1)
PB_IN_GGAG(X1, X2, X3, X4) → U3_GGAG(X1, X2, X3, X4, appendcC_in_gga(X1, X2, X3))
U3_GGAG(X1, X2, X3, X4, appendcC_out_gga(X1, X2, X3)) → LESSLEAVESA_IN_GG(X4, X3)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U7_GG(X1, X2, X3, X4, X5, appendcC_in_gga(X2, X3, X6))
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → PB_IN_GGAG(X4, X5, X7, cons(X1, X6))
appendcC_in_gga(nil, X1, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3, cons(X1, X4)) → U13_gga(X1, X2, X3, X4, appendcC_in_gga(X2, X3, X4))
U13_gga(X1, X2, X3, X4, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → PB_IN_GGAG(X2, X3, X1)
PB_IN_GGAG(X1, X2, X4) → U3_GGAG(X1, X2, X4, appendcC_in_gga(X1, X2))
U3_GGAG(X1, X2, X4, appendcC_out_gga(X1, X2, X3)) → LESSLEAVESA_IN_GG(X4, X3)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U7_GG(X1, X2, X3, X4, X5, appendcC_in_gga(X2, X3))
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → PB_IN_GGAG(X4, X5, cons(X1, X6))
appendcC_in_gga(nil, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3) → U13_gga(X1, X2, X3, appendcC_in_gga(X2, X3))
U13_gga(X1, X2, X3, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
appendcC_in_gga(x0, x1)
U13_gga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LESSLEAVESA_IN_GG(cons(nil, X1), cons(X2, X3)) → PB_IN_GGAG(X2, X3, X1)
LESSLEAVESA_IN_GG(cons(cons(X1, X2), X3), cons(X4, X5)) → U7_GG(X1, X2, X3, X4, X5, appendcC_in_gga(X2, X3))
POL(LESSLEAVESA_IN_GG(x1, x2)) = 1 + x2
POL(PB_IN_GGAG(x1, x2, x3)) = x1 + x2
POL(U13_gga(x1, x2, x3, x4)) = x1 + x4
POL(U3_GGAG(x1, x2, x3, x4)) = x4
POL(U7_GG(x1, x2, x3, x4, x5, x6)) = x4 + x5
POL(appendcC_in_gga(x1, x2)) = x1 + x2
POL(appendcC_out_gga(x1, x2, x3)) = 1 + x3
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 1
appendcC_in_gga(nil, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3) → U13_gga(X1, X2, X3, appendcC_in_gga(X2, X3))
U13_gga(X1, X2, X3, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
PB_IN_GGAG(X1, X2, X4) → U3_GGAG(X1, X2, X4, appendcC_in_gga(X1, X2))
U3_GGAG(X1, X2, X4, appendcC_out_gga(X1, X2, X3)) → LESSLEAVESA_IN_GG(X4, X3)
U7_GG(X1, X2, X3, X4, X5, appendcC_out_gga(X2, X3, X6)) → PB_IN_GGAG(X4, X5, cons(X1, X6))
appendcC_in_gga(nil, X1) → appendcC_out_gga(nil, X1, X1)
appendcC_in_gga(cons(X1, X2), X3) → U13_gga(X1, X2, X3, appendcC_in_gga(X2, X3))
U13_gga(X1, X2, X3, appendcC_out_gga(X2, X3, X4)) → appendcC_out_gga(cons(X1, X2), X3, cons(X1, X4))
appendcC_in_gga(x0, x1)
U13_gga(x0, x1, x2, x3)